CPAchecker Report

Find only exact matches

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

	Rank	Scope
-V-		{{line.bestrank}}		{{line.desc}}

Precondition (initial variable assignment):

{{fault.rank}}.

Details:

Current values:

Name	Value

{{sourceFiles[selectedSourceFile]}}

typedef enum { false, true } bool;  
  
extern int __VERIFIER_nondet_int(void);  
  
int main() {  
    int i;  
    int up;  
    i = __VERIFIER_nondet_int();  
    up = 0;  
      
    while (i > 0) {  
        if (i == 1) {  
            up = 1;  
        }  
        if (i == 10) {  
            up = 0;  
        }  
        if (up == 1) {  
            i = i+1;  
        } else {  
            i = i-1;  
        }  
    }  
      
    return 0;  
}  

DateTimeLevelComponentMessage
2025-08-2713:26:10:820INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2025-08-2713:26:10:905INFOCPAchecker.runCPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started
2025-08-2713:26:10:924INFOCPAchecker.parseParsing CFA from file(s) "Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c"
2025-08-2713:26:11:901INFOCoreComponentsFactory.createAlgorithmUsing Restarting Algorithm
2025-08-2713:26:11:923WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
 cpa.arg.lateMerge
 counterexample.export.exportWitness 
2025-08-2713:26:11:924INFOCPAchecker.runAlgorithmStarting analysis ...
2025-08-2713:26:11:931INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ...
2025-08-2713:26:11:976INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
ResourceLimitChecker.fromConfigurationUsing the following resource limits: Thread CPU-time limit of 300s
2025-08-2713:26:12:355INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPA.<init>Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2713:26:12:670INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPARefiner.<init>Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2713:26:12:680WARNINGCPAs.retrieveCPAOrFailWarning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA)
2025-08-2713:26:12:682INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ...
2025-08-2713:26:12:692INFONestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'.
2025-08-2713:26:12:717WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
FormulaManagerView.<init>Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2713:26:12:721INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPA.<init>Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2713:26:12:831INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPARefiner.<init>Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2713:26:12:896WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
FormulaManagerView.<init>Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2713:26:12:932INFORestartAlgorithm.runStarting analysis 1 ...
2025-08-2713:26:12:933INFOAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.run0Starting termination algorithm.
2025-08-2713:26:17:236WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:18:693WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:20:373WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:21:957WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:23:698WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:25:628WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:27:110WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:28:811WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:30:002WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:31:640WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:33:472WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:34:712WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:36:430WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:38:276WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:40:086WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:41:304WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:43:832WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:45:357WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:46:675WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:48:379WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:49:678WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:51:328WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:53:021WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:55:743WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:57:129WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:26:58:810WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:02:246WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:03:709WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:06:558WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:08:641WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:10:046WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:11:987WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:13:935WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:16:828WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:18:186WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:20:134WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:23:510WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:25:121WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:27:603WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:30:411WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:32:361WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:35:022WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:37:234WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:40:853WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:42:174WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:44:758WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:48:437WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:50:060WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:53:075WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:54:824WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:57:949WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:27:59:661WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:01:745WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:03:367WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:06:977WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:08:890WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:10:533WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:13:034WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:14:637WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:19:597WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:21:672WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:23:502WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:25:588WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:27:248WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:28:953WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTerminationCould not synthesize a termination or non-termination argument.
2025-08-2713:28:29:593INFOAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheckAlgorithm.checkCounterexampleError path found, starting counterexample check with CPACHECKER.
2025-08-2713:28:30:047WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheck
AutomatonGraphmlParser.getSpecAsPropertiesCannot map specification TRUE to property type. Will ignore it (would only be problematic if this were the termination property).
2025-08-2713:28:30:081WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheck
AutomatonGraphmlParser.collectEdgeDataSource A17144 of transition [edge: null] is a violation state. No outgoing edges expected.
2025-08-2713:28:30:136INFOAnalysis /cpachecker/config/components/termination-recursion.properties
CounterexampleCheck
PredicateCPA
PredicateCPA.<init>Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-08-2713:41:09:404WARNINGShutdownNotifier.shutdownIfNecessaryWarning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.)
2025-08-2713:41:09:406WARNINGForceTerminationOnShutdown$1.shutdownRequestedShutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination.

        

Date	Time	Level	Component	Message
2025-08-27	13:26:10:820	INFO	CPAMain.detectFrontendLanguageIfNecessary	Language C detected and set for analysis
2025-08-27	13:26:10:905	INFO	CPAchecker.run	CPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started
2025-08-27	13:26:10:924	INFO	CPAchecker.parse	Parsing CFA from file(s) "Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c"
2025-08-27	13:26:11:901	INFO	CoreComponentsFactory.createAlgorithm	Using Restarting Algorithm
2025-08-27	13:26:11:923	WARNING	CPAchecker.printConfigurationWarnings	The following configuration options were specified but are not used: cpa.arg.lateMerge counterexample.export.exportWitness
2025-08-27	13:26:11:924	INFO	CPAchecker.runAlgorithm	Starting analysis ...
2025-08-27	13:26:11:931	INFO	RestartAlgorithm.run	Loading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ...
2025-08-27	13:26:11:976	INFO	Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 ResourceLimitChecker.fromConfiguration	Using the following resource limits: Thread CPU-time limit of 300s
2025-08-27	13:26:12:355	INFO	Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPA.<init>	Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-27	13:26:12:670	INFO	Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPARefiner.<init>	Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-27	13:26:12:680	WARNING	CPAs.retrieveCPAOrFail	Warning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA)
2025-08-27	13:26:12:682	INFO	RestartAlgorithm.run	Loading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ...
2025-08-27	13:26:12:692	INFO	NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'.
2025-08-27	13:26:12:717	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA FormulaManagerView.<init>	Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-27	13:26:12:721	INFO	Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPA.<init>	Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-27	13:26:12:831	INFO	Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPARefiner.<init>	Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-27	13:26:12:896	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties FormulaManagerView.<init>	Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-27	13:26:12:932	INFO	RestartAlgorithm.run	Starting analysis 1 ...
2025-08-27	13:26:12:933	INFO	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.run0	Starting termination algorithm.
2025-08-27	13:26:17:236	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:18:693	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:20:373	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:21:957	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:23:698	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:25:628	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:27:110	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:28:811	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:30:002	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:31:640	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:33:472	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:34:712	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:36:430	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:38:276	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:40:086	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:41:304	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:43:832	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:45:357	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:46:675	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:48:379	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:49:678	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:51:328	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:53:021	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:55:743	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:57:129	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:26:58:810	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:02:246	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:03:709	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:06:558	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:08:641	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:10:046	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:11:987	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:13:935	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:16:828	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:18:186	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:20:134	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:23:510	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:25:121	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:27:603	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:30:411	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:32:361	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:35:022	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:37:234	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:40:853	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:42:174	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:44:758	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:48:437	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:50:060	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:53:075	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:54:824	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:57:949	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:27:59:661	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:01:745	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:03:367	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:06:977	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:08:890	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:10:533	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:13:034	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:14:637	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:19:597	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:21:672	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:23:502	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:25:588	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:27:248	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:28:953	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination	Could not synthesize a termination or non-termination argument.
2025-08-27	13:28:29:593	INFO	Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheckAlgorithm.checkCounterexample	Error path found, starting counterexample check with CPACHECKER.
2025-08-27	13:28:30:047	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheck AutomatonGraphmlParser.getSpecAsProperties	Cannot map specification TRUE to property type. Will ignore it (would only be problematic if this were the termination property).
2025-08-27	13:28:30:081	WARNING	Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheck AutomatonGraphmlParser.collectEdgeData	Source A17144 of transition [edge: null] is a violation state. No outgoing edges expected.
2025-08-27	13:28:30:136	INFO	Analysis /cpachecker/config/components/termination-recursion.properties CounterexampleCheck PredicateCPA PredicateCPA.<init>	Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant).
2025-08-27	13:41:09:404	WARNING	ShutdownNotifier.shutdownIfNecessary	Warning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.)
2025-08-27	13:41:09:406	WARNING	ForceTerminationOnShutdown$1.shutdownRequested	Shutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination.

Statistics NameStatistics ValueAdditional Value
Restart Algorithm statistics
Number of algorithms provided    2
Number of algorithms used        1
Last algorithm used        /cpachecker/config/components/combinations-parallel-termination.properties
Total time for algorithm 1   897.471s
PredicateCPA statistics
Number of abstractions            728 5% of all post computations
	  Times abstraction was reused    0
	  Because of function entry/exit  0 0%
	  Because of loop head            397 55%
	  Because of join nodes           0 0%
	  Because of threshold            0 0%
	  Because of target state         331 45%
	  Times precision was empty       11 2%
	  Times precision was {false}     328 45%
	  Times result was cached         1 0%
	  Times cartesian abs was used    0 0%
	  Times boolean abs was used      388 53%
	  Times result was 'false'        249 34%
Number of strengthen sat checks   0
Number of coverage checks         182099
	  BDD entailment checks           11846
Number of SMT sat checks          0
	  trivial                         0
	  cached                          0
Max ABE block size                       13
Avg ABE block size                                6.39 sum: 4650, count: 728, min: 0, max: 13
Number of predicates discovered          93
Number of abstraction locations          2
Max number of predicates per location    93
Avg number of predicates per location    47
Total predicates per abstraction         26260
Max number of predicates per abstraction 93
Avg number of predicates per abstraction 36.68
Number of irrelevant predicates          805 3%
Number of preds handled by boolean abs   25451 97%
	  Total number of models for allsat      27593
	  Max number of models for allsat        1275
	  Avg number of models for allsat        71.12
Time for post operator                                1.229s
	  Time for path formula creation                      1.214s
Time for strengthen operator                          0.258s
Time for prec operator                               21.150s
	  Time for abstraction                 21.019s Max:     1.001s, Count: 728
		    Boolean abstraction                16.907s
		    Solving time                        2.110s Max:     0.013s
		    Model enumeration time             15.098s
		    Time for BDD construction           4.118s Max:     0.038s
Time for merge operator                               0.071s
Time for coverage checks                              0.119s
	  Time for BDD entailment checks                      0.101s
Total time for SMT solver (w/o itp)    17.208s
Number of path formula cache hits   9652 48%
Inside post operator                  
	  Inside path formula creation        
		    Time for path formula computation     1.179s
Total number of created targets for pointer analysis 0
Number of BDD nodes                               205476
Size of BDD node table                            466043
Size of BDD cache                                 46619
Size of BDD node cleanup queue                    2.16 sum: 262783, count: 121752, min: 0, max: 16573
Time for BDD node cleanup                             0.036s
Time for BDD garbage collection                       0.172s in 52 runs
KeyValue statistics
Init. function predicates                         0
Init. global predicates                           0
Init. location predicates                         0
Invariant Generation statistics
AutomatonAnalysis (NonTerminationLabelAutomaton) statistics
Number of states                                  1
Total time for successor computation                  0.172s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966]
Number of states with assumption transitions      0
AutomatonAnalysis (TerminatingFunctions) statistics
Number of states                                  1
Total time for successor computation                  0.019s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966]
Number of states with assumption transitions      0
Termination Algorithm statistics
Total time                                           136.637s
Time for recursion analysis                            0.000s
Number of analysed loops                               1 100%
Total time for loop analysis                         136.630s
	  Avg time per loop analysis                         136.630s
	  Max time per loop analysis                         136.630s
Number of safety analysis runs                        70
	  Avg safety analysis run per loop                    70.00
	  Max safety analysis run per loop                    70 	 for loops [N7]
Total time for safety analysis                        28.061s
	  Avg time per safety analysis run                     0.400s
	  Max time per safety analysis run                     1.464s
Number of analysed lassos                             71
	  Avg number of lassos per loop                       71.00
	  Max number of lassos per loop                       71 	 for loops [N7]
	  Avg number of lassos per iteration                   1.01
	  Max number of lassos per iteration                   2
Total time for lassos analysis                       108.385s
	  Avg time per iteration                               1.548s
	  Max time per iteration                               4.561s
	  Time for lassos construction                         4.519s
		    Avg time for lasso construction per iteration      0.064s
		    Max time for lasso construction per iteration      0.358s
			      Time for stem and loop construction                         0.279s
				        Avg time for stem and loop construction per iteration      0.003s
				        Max time for stem and loop construction per iteration      0.030s
			      Time for lassos creation                         4.237s
				        Avg time for lassos creation per iteration      0.060s
				        Max time for lassos creation per iteration      0.357s
	  Total time for non-termination analysis              9.402s
		    Avg time for non-termination analysis per lasso    0.132s
		    Max time for non-termination analysis per lasso    0.173s
	  Total time for termination analysis                 94.463s
		    Avg time for termination analysis per lasso        1.349s
		    Max time for termination analysis per lasso        4.330s
Total number of termination arguments                  5
	  Avg termination arguments per loop                   5.00
	  Max termination arguments per loop                   5 	 for loops [N7]
	  affine                                               5
Counterexample-Check Algorithm statistics
Number of counterexample checks    1
Number of infeasible paths         0 0%
Time for counterexample checks       759.813s
Termination Algorithm statistics
Total time                                           136.637s
Time for recursion analysis                            0.000s
Number of analysed loops                               1 100%
Total time for loop analysis                         136.630s
	  Avg time per loop analysis                         136.630s
	  Max time per loop analysis                         136.630s
Number of safety analysis runs                        70
	  Avg safety analysis run per loop                    70.00
	  Max safety analysis run per loop                    70 	 for loops [N7]
Total time for safety analysis                        28.061s
	  Avg time per safety analysis run                     0.400s
	  Max time per safety analysis run                     1.464s
Number of analysed lassos                             71
	  Avg number of lassos per loop                       71.00
	  Max number of lassos per loop                       71 	 for loops [N7]
	  Avg number of lassos per iteration                   1.01
	  Max number of lassos per iteration                   2
Total time for lassos analysis                       108.385s
	  Avg time per iteration                               1.548s
	  Max time per iteration                               4.561s
	  Time for lassos construction                         4.519s
		    Avg time for lasso construction per iteration      0.064s
		    Max time for lasso construction per iteration      0.358s
			      Time for stem and loop construction                         0.279s
				        Avg time for stem and loop construction per iteration      0.003s
				        Max time for stem and loop construction per iteration      0.030s
			      Time for lassos creation                         4.237s
				        Avg time for lassos creation per iteration      0.060s
				        Max time for lassos creation per iteration      0.357s
	  Total time for non-termination analysis              9.402s
		    Avg time for non-termination analysis per lasso    0.132s
		    Max time for non-termination analysis per lasso    0.173s
	  Total time for termination analysis                 94.463s
		    Avg time for termination analysis per lasso        1.349s
		    Max time for termination analysis per lasso        4.330s
Total number of termination arguments                  5
	  Avg termination arguments per loop                   5.00
	  Max termination arguments per loop                   5 	 for loops [N7]
	  affine                                               5
Counterexample-Check Algorithm statistics
Number of counterexample checks    1
Number of infeasible paths         0 0%
Time for counterexample checks       759.813s
Code Coverage
	  Function coverage      1.000
	  Visited lines          14
	  Total lines            14
	  Line coverage          1.000
	  Visited conditions     8
	  Total conditions       8
	  Condition coverage     1.000
CPAchecker general statistics
Number of program locations                       26
Number of CFA edges (per node)                          29 count: 26, min: 0, max: 2, avg: 1.12
Number of relevant variables                      2
Number of functions                               1
Number of loops (and loop nodes)                         1 sum: 13, min: 13, max: 13, avg: 13.00
Size of reached set             1812
	  Number of reached locations   18 69%
		    Avg states per location     100
		    Max states per location     146 at node N8
	  Number of reached functions   1 100%
	  Number of partitions          18
		    Avg size of partitions      100
		    Max size of partitions      146 with key N8
	  Number of target states       1
	  Size of final wait list       10
Time for analysis setup          0.999s
	  Time for loading CPAs          0.016s
	  Time for loading parser        0.227s
	  Time for CFA construction      0.707s
		    Time for parsing file(s)     0.256s
		    Time for AST to CFA          0.172s
		    Time for CFA sanity check    0.019s
		    Time for post-processing     0.121s
		    Time for loop structure      0.005s
		    Time for AST structure       0.000s
		    Time for CFA export          0.429s
			      Time for function pointers resolving            0.003s
				        Function calls via function pointers             0 count: 1, min: 0, max: 0, avg: 0.00
				        Instrumented function pointer calls              0 count: 1, min: 0, max: 0, avg: 0.00
				        Function calls with function pointer arguments        0 count: 1, min: 0, max: 0, avg: 0.00
				        Instrumented function pointer arguments          0 count: 1, min: 0, max: 0, avg: 0.00
			      Time for classifying variables                  0.076s
				        Time for collecting variables                 0.049s
				        Time for solving dependencies                 0.003s
				        Time for building hierarchy                   0.000s
				        Time for building classification              0.020s
				        Time for exporting data                       0.003s
Time for Analysis              897.472s
CPU time for analysis          850.940s
Total time for CPAchecker      898.481s
Total CPU time for CPAchecker  852.620s
Time for statistics              0.672s
Time for Garbage Collector       3.269s in 1952 runs
Garbage Collector(s) used    PS MarkSweep, PS Scavenge
Used heap memory                372MB (   355 MiB) max;    272MB (   260 MiB) avg;    444MB (   423 MiB) peak
Used non-heap memory             73MB (    70 MiB) max;     70MB (    66 MiB) avg;     74MB (    70 MiB) peak
Used in PS Old Gen pool         341MB (   325 MiB) max;    255MB (   243 MiB) avg;    352MB (   336 MiB) peak
Allocated heap memory           821MB (   783 MiB) max;    692MB (   660 MiB) avg
Allocated non-heap memory        75MB (    71 MiB) max;     73MB (    70 MiB) avg
Total process virtual memory  16365MB ( 15607 MiB) max;  16273MB ( 15519 MiB) avg

        

Statistics Name	Statistics Value	Additional Value
Restart Algorithm statistics
Number of algorithms provided	2
Number of algorithms used	1
Last algorithm used	/cpachecker/config/components/combinations-parallel-termination.properties
Total time for algorithm 1	897.471s
PredicateCPA statistics
Number of abstractions	728	5% of all post computations
Times abstraction was reused	0
Because of function entry/exit	0	0%
Because of loop head	397	55%
Because of join nodes	0	0%
Because of threshold	0	0%
Because of target state	331	45%
Times precision was empty	11	2%
Times precision was {false}	328	45%
Times result was cached	1	0%
Times cartesian abs was used	0	0%
Times boolean abs was used	388	53%
Times result was 'false'	249	34%
Number of strengthen sat checks	0
Number of coverage checks	182099
BDD entailment checks	11846
Number of SMT sat checks	0
trivial	0
cached	0
Max ABE block size	13
Avg ABE block size	6.39	sum: 4650, count: 728, min: 0, max: 13
Number of predicates discovered	93
Number of abstraction locations	2
Max number of predicates per location	93
Avg number of predicates per location	47
Total predicates per abstraction	26260
Max number of predicates per abstraction	93
Avg number of predicates per abstraction	36.68
Number of irrelevant predicates	805	3%
Number of preds handled by boolean abs	25451	97%
Total number of models for allsat	27593
Max number of models for allsat	1275
Avg number of models for allsat	71.12
Time for post operator	1.229s
Time for path formula creation	1.214s
Time for strengthen operator	0.258s
Time for prec operator	21.150s
Time for abstraction	21.019s	Max: 1.001s, Count: 728
Boolean abstraction	16.907s
Solving time	2.110s	Max: 0.013s
Model enumeration time	15.098s
Time for BDD construction	4.118s	Max: 0.038s
Time for merge operator	0.071s
Time for coverage checks	0.119s
Time for BDD entailment checks	0.101s
Total time for SMT solver (w/o itp)	17.208s
Number of path formula cache hits	9652	48%
Inside post operator
Inside path formula creation
Time for path formula computation	1.179s
Total number of created targets for pointer analysis	0
Number of BDD nodes	205476
Size of BDD node table	466043
Size of BDD cache	46619
Size of BDD node cleanup queue	2.16	sum: 262783, count: 121752, min: 0, max: 16573
Time for BDD node cleanup	0.036s
Time for BDD garbage collection	0.172s	in 52 runs
KeyValue statistics
Init. function predicates	0
Init. global predicates	0
Init. location predicates	0
Invariant Generation statistics
AutomatonAnalysis (NonTerminationLabelAutomaton) statistics
Number of states	1
Total time for successor computation	0.172s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966]
Number of states with assumption transitions	0
AutomatonAnalysis (TerminatingFunctions) statistics
Number of states	1
Total time for successor computation	0.019s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 13966, count: 13966, min: 1, max: 1 [1 x 13966]
Number of states with assumption transitions	0
Termination Algorithm statistics
Total time	136.637s
Time for recursion analysis	0.000s
Number of analysed loops	1	100%
Total time for loop analysis	136.630s
Avg time per loop analysis	136.630s
Max time per loop analysis	136.630s
Number of safety analysis runs	70
Avg safety analysis run per loop	70.00
Max safety analysis run per loop	70 for loops [N7]
Total time for safety analysis	28.061s
Avg time per safety analysis run	0.400s
Max time per safety analysis run	1.464s
Number of analysed lassos	71
Avg number of lassos per loop	71.00
Max number of lassos per loop	71 for loops [N7]
Avg number of lassos per iteration	1.01
Max number of lassos per iteration	2
Total time for lassos analysis	108.385s
Avg time per iteration	1.548s
Max time per iteration	4.561s
Time for lassos construction	4.519s
Avg time for lasso construction per iteration	0.064s
Max time for lasso construction per iteration	0.358s
Time for stem and loop construction	0.279s
Avg time for stem and loop construction per iteration	0.003s
Max time for stem and loop construction per iteration	0.030s
Time for lassos creation	4.237s
Avg time for lassos creation per iteration	0.060s
Max time for lassos creation per iteration	0.357s
Total time for non-termination analysis	9.402s
Avg time for non-termination analysis per lasso	0.132s
Max time for non-termination analysis per lasso	0.173s
Total time for termination analysis	94.463s
Avg time for termination analysis per lasso	1.349s
Max time for termination analysis per lasso	4.330s
Total number of termination arguments	5
Avg termination arguments per loop	5.00
Max termination arguments per loop	5 for loops [N7]
affine	5
Counterexample-Check Algorithm statistics
Number of counterexample checks	1
Number of infeasible paths	0	0%
Time for counterexample checks	759.813s
Termination Algorithm statistics
Total time	136.637s
Time for recursion analysis	0.000s
Number of analysed loops	1	100%
Total time for loop analysis	136.630s
Avg time per loop analysis	136.630s
Max time per loop analysis	136.630s
Number of safety analysis runs	70
Avg safety analysis run per loop	70.00
Max safety analysis run per loop	70 for loops [N7]
Total time for safety analysis	28.061s
Avg time per safety analysis run	0.400s
Max time per safety analysis run	1.464s
Number of analysed lassos	71
Avg number of lassos per loop	71.00
Max number of lassos per loop	71 for loops [N7]
Avg number of lassos per iteration	1.01
Max number of lassos per iteration	2
Total time for lassos analysis	108.385s
Avg time per iteration	1.548s
Max time per iteration	4.561s
Time for lassos construction	4.519s
Avg time for lasso construction per iteration	0.064s
Max time for lasso construction per iteration	0.358s
Time for stem and loop construction	0.279s
Avg time for stem and loop construction per iteration	0.003s
Max time for stem and loop construction per iteration	0.030s
Time for lassos creation	4.237s
Avg time for lassos creation per iteration	0.060s
Max time for lassos creation per iteration	0.357s
Total time for non-termination analysis	9.402s
Avg time for non-termination analysis per lasso	0.132s
Max time for non-termination analysis per lasso	0.173s
Total time for termination analysis	94.463s
Avg time for termination analysis per lasso	1.349s
Max time for termination analysis per lasso	4.330s
Total number of termination arguments	5
Avg termination arguments per loop	5.00
Max termination arguments per loop	5 for loops [N7]
affine	5
Counterexample-Check Algorithm statistics
Number of counterexample checks	1
Number of infeasible paths	0	0%
Time for counterexample checks	759.813s
Code Coverage
Function coverage	1.000
Visited lines	14
Total lines	14
Line coverage	1.000
Visited conditions	8
Total conditions	8
Condition coverage	1.000
CPAchecker general statistics
Number of program locations	26
Number of CFA edges (per node)	29	count: 26, min: 0, max: 2, avg: 1.12
Number of relevant variables	2
Number of functions	1
Number of loops (and loop nodes)	1	sum: 13, min: 13, max: 13, avg: 13.00
Size of reached set	1812
Number of reached locations	18	69%
Avg states per location	100
Max states per location	146	at node N8
Number of reached functions	1	100%
Number of partitions	18
Avg size of partitions	100
Max size of partitions	146	with key N8
Number of target states	1
Size of final wait list	10
Time for analysis setup	0.999s
Time for loading CPAs	0.016s
Time for loading parser	0.227s
Time for CFA construction	0.707s
Time for parsing file(s)	0.256s
Time for AST to CFA	0.172s
Time for CFA sanity check	0.019s
Time for post-processing	0.121s
Time for loop structure	0.005s
Time for AST structure	0.000s
Time for CFA export	0.429s
Time for function pointers resolving	0.003s
Function calls via function pointers	0	count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls	0	count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables	0.076s
Time for collecting variables	0.049s
Time for solving dependencies	0.003s
Time for building hierarchy	0.000s
Time for building classification	0.020s
Time for exporting data	0.003s
Time for Analysis	897.472s
CPU time for analysis	850.940s
Total time for CPAchecker	898.481s
Total CPU time for CPAchecker	852.620s
Time for statistics	0.672s
Time for Garbage Collector	3.269s	in 1952 runs
Garbage Collector(s) used	PS MarkSweep, PS Scavenge
Used heap memory	372MB ( 355 MiB) max; 272MB ( 260 MiB) avg; 444MB ( 423 MiB) peak
Used non-heap memory	73MB ( 70 MiB) max; 70MB ( 66 MiB) avg; 74MB ( 70 MiB) peak
Used in PS Old Gen pool	341MB ( 325 MiB) max; 255MB ( 243 MiB) avg; 352MB ( 336 MiB) peak
Allocated heap memory	821MB ( 783 MiB) max; 692MB ( 660 MiB) avg
Allocated non-heap memory	75MB ( 71 MiB) max; 73MB ( 70 MiB) avg
Total process virtual memory	16365MB ( 15607 MiB) max; 16273MB ( 15519 MiB) avg

#Configuration NameConfiguration Value
1analysis.algorithm.termination  true
2analysis.machineModel  Linux64
3analysis.name  terminationAnalysis
4analysis.programNames  Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c
5analysis.restartAfterUnknown  true
6counterexample.export.exportWitness  false
7cpa.arg.lateMerge  prevent
8language  C
9log.level  INFO
10parser.usePreprocessor  true
11restartAlgorithm.configFiles  components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive
12specification  
13statistics.print  true
14termination.config  terminationAnalysis.properties

        

#	Configuration Name	Configuration Value
1	analysis.algorithm.termination	true
2	analysis.machineModel	Linux64
3	analysis.name	terminationAnalysis
4	analysis.programNames	Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c
5	analysis.restartAfterUnknown	true
6	counterexample.export.exportWitness	false
7	cpa.arg.lateMerge	prevent
8	language	C
9	log.level	INFO
10	parser.usePreprocessor	true
11	restartAlgorithm.configFiles	components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive
12	specification
13	statistics.print	true
14	termination.config	terminationAnalysis.properties

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

Source: {{dependency.repository}}

License:

Full text of license

{{dependencies.licenses[dependency.licenseId]}}

Report for Benchmarks/TermCOMP/C/Stroeder_15/Ex08/Ex08.c (Counterexample 141)

About

{{dependency.name}} {{dependency.version}}

1	typedef enum { false, true } bool;
2
3	extern int __VERIFIER_nondet_int(void);
4
5	int main() {
6	int i;
7	int up;
8	i = __VERIFIER_nondet_int();
9	up = 0;
10
11	while (i > 0) {
12	if (i == 1) {
13	up = 1;
14	}
15	if (i == 10) {
16	up = 0;
17	}
18	if (up == 1) {
19	i = i+1;
20	} else {
21	i = i-1;
22	}
23	}
24
25	return 0;
26	}